\lstset{
   escapechar=`,
   extendedchars=\true,
   keywords={},
   sensitive=true,
   basicstyle=\small,
   commentstyle=\scriptsize\rmfamily,
   keywordstyle=\ttfamily\underbar,
   identifierstyle=\ttfamily,
   basewidth={0.5em,0.5em},
   columns=fixed,
   fontadjust=true,
   literate={->}{{$\to$}}1 {>>}{{$\gg$}}1 {<<}{{$\ll$}}1
}

\newcommand{\ctab}[0]{\indent\indent}
\newcommand{\ctabd}[0]{\ctab\ctab}
\newcommand{\ccode}[1]{\mbox{\texttt{#1}}}

\newcommand{\lcode}[1]{\lstinline{#1}}

\title{Использование proof assistants для описания операционных семантик}
%
\titlerunning{Использование proof assistants}
\author{Таран Кирилл Сергеевич}
%
%\authorrunning{К.С.Таран} % abbreviated author list (for running head)
%
%%%% list of authors for the TOC (use if author list has to be modified)
\tocauthor{К.С.Таран}
%
\institute{Санкт-Петербургский государственный университет\\
\email{kirill.t256@gmail.com}}

\maketitle              % typeset the title of the contribution

\begin{abstract}
В работе описывается применение средств автоматизации построения доказательств (proof
assistants) для описания операционной семантики языков программирования и доказательства
некоторых её свойств.
\end{abstract}

\vskip 5mm

\section*{Введение}

     В данной работе будут рассмотрены возможности систем для интерактивного доказательство теорем (далее \emph{proof assistants}) применительно к описанию операционных семантик --- дедуктивных систем, описывающих поведение программ, написанных на языке программирования.

     \emph{Операционные семантики} --- один из способов формально описать семантику языка. С их помощью можно описывать интерпретаторы, компиляторы, статические анализаторы и прочие программы, необходимые для работы с языками программирования, таким образом, что о них можно рассуждать формально. В свою очередь, формализация разрабатываемого объекта даёт возможность снизить количество ошибок при реализации, верфицировать полученную программу (т.е. доказать её корректность), а в некоторых случаях и автоматизировать сам процесс разработки.

     В то же время, \emph{сертификационное программирование} --- направление, в котором при разработке программы используются формальные описания и доказательства её полезных или других интересных свойств. Появилось это направление в связи с развитием средств для интерактивного доказательства и автоматической проверки теорем. Относительно новое поколение таких средств основано на \emph{зависимых типах} и позволяет совместить программу и доказательство её корректности в одном тексте.

     Цель данной работы --- оценить применимость proof assistants в области разработки языков программирования, в частности для:
     \begin{itemize}
        \item описания операционной семантики;
        \item автоматизированной генерации интерпретатора по операционной семантике (встроенными средствами выбранного инструмента);
        \item доказательствa каких-либо свойств об интерпретации (по возможности автоматического).
     \end{itemize}

  \section{Обзор proof assistants}

     В данной работе сделан упор на поколении proof assistants, в основе реализации которых лежит язык программирования с зависимыми типами.

     Такие системы позволяют кодировать утверждения теорем и их доказательства средствами самого языка, используя соответствие Карри-Говарда. Поэтому proof assistants на зависимых типах являются примером применения стройной математической теории в программировании. 

  \subsection{Зависимые типы}

     \setlength{\epigraphwidth}{10cm}
     \epigraph{Система типов --- это гибко управляемый синтаксический метод доказательства отсутствия в программе определённых видов поведения при помощи классификации выражений языка по разновидностям вычисляемых ими значений.}{``Types and Programming Languages''\cite{Pierce:2002:TPL:509043}}

     Механизм \emph{зависимых типов} является расширением параметрического полиморфизма.

     При наличии параметрического полиморфизма в языке мы можем работать с типами, параметризованными другими типами. В качестве примера приведём \lcode{List A}\:--- тип списка с элементами типа \lcode{A}.

     Код, определяющий этот тип данных:
     \begin{lstlisting}
     data List (A : Set) : Set where
       cons : A -> List A -> List A
       nil  : List A
     \end{lstlisting}

     Примером параметрического полиморфизма могут служить также \emph{generics} в Java и С\#. Подробнее про параметричекий полиморфизм можно прочитать в \cite{DBLP:journals/lisp/Strachey00}.

     Зависимые же типы могут быть параметризованы не только типами, но и термами (значениями). Классический пример зависимого типа: \lcode{Vector A (n : N)}\:--- список фиксированной длины n.

     Код, определяющий этот тип данных:
     \begin{lstlisting}
     data Vector (A : Set) : N -> Set where
       cons : (n : N) -> A -> Vector A n -> Vector A (S n)
       nil  : Vector A O
     -- S - конструктор` `ненулевых` `натуральных` `чисел
     -- S n == n + 1
     \end{lstlisting}
     
     Возможность использования термов в качестве типовых параметров позволяет записывать предикаты как типы, а значит, можно использовать предикаты как типы аргументов функций.

     Частично примером может служить функция \lcode{head} с типом \lcode{(n : N) -> Vector A (S n) -> A}, возвращающая первый элемент списка типа \lcode{Vector}. Эта функция ожидает в качестве аргумента терм типа \lcode{Vector A (S n)}, что исключает воможность вызвать \lcode{head} от пустого списка.

     Числа \lcode{(S n)} здесь являются конструктивными доказательствами предиката ``список не пуст''. Этот предикат задан неявно, как часть определения типа \lcode{Vector}, но возможно и явное задание в виде обособленного типа вроде \lcode{Predicate (p : Proof)} с доказательствами его выполнения в виде элементов типа \lcode{Proof}.

     Описания подобных приёмов можно почерпнуть из \cite{DBLP:conf/tldi/Norell09}.

     Другая идиома, которую открывают зависимые типы --- \emph{представления} (\emph{views}). Она заключается в особом описании типов с параметрами таким образом, что сопоставление элементов этих типов с образцом сообщает дополнительную информацию об элементе-параметре.

     Пример:
     \begin{lstlisting}
     data Parity : N -> Set where
       even : (k : N) -> Parity (k * 2)
       odd  : (k : N) -> Parity (k * 2 + 1)
     \end{lstlisting}

     Далее мы можем использовать элементы типа \lcode{Parity} для некоторого числа n, чтобы разложить аргумент n некоторой функции либо на \lcode{k * 2}, либо на \lcode{k * 2 + 1} в зависимости от значения \lcode{parity} для n:
     \begin{lstlisting}
     f : N -> ...
     f n with parity n -- parity : (n : N) -> Parity n
     f .(k * 2)     | even k = ...
     f .(k * 2 + 1) | odd  k = ...
     -- точка` `означает` `автоматически` `выводимый` `шаблон
     \end{lstlisting}

     В дальнейшем эта техника будет использована для описания операционной семантики.
     
  \subsection{Соответствие Карри-Говарда}

     Соответствие Карри-Говарда --- наблюдаемое структурное сходство между компьютерными программами и математическими доказательствами. Его суть состоит в том, что любой типизированной системе соответствует некоторая логика, и наоборот.

     Именно благодаря этому соответствию мы можем использовать зависимые типы для выражения условий. Можно сказать, что высказывания есть типы, а их доказательства являются программами.

     Известная книга Б. Пирса по теории типов так объясняет зависимые типы: ``В конструктивных логиках доказательство утверждения $P$ состоит в демонстрации конкретного \emph{свидетельства} в пользу $P$. Карри и Говард заметили, что это свидетельство во многом похоже на вычисление. Например, доказательство утверждения $P \Rightarrow Q$ можно рассматривать как механическую процедуру, которая, получая доказательство $P$, строит доказательство $Q$.''\cite{Pierce:2002:TPL:509043}

     В рамках соответствия Карри-Говарда следующие структурные элементы рассматриваются как аналогичные:
     \begin{align*}
        \small
        \begin{tabular}{l || r}
           высказывание $P$                & тип \ccode{P}         \\
           доказательство высказывания $P$ & терм типа \ccode{P}   \\
           утверждение $P$ доказуемо       & тип \ccode{P} обитаем \\
           конъюнкция $P \wedge Q$         & кортеж \ccode{P $\times$ Q} \\
           дизъюнкция $P \vee Q$           & размеченное объединение \ccode{P $+$ Q} \\
           импликация $P \Rightarrow Q$    & функциональный тип \ccode{P $\to$ Q} \\
           истинная формула                & тип с единственным элементом \\
           ложная формула                  & тип без элементов \\
           квантор всеобщности $\forall$   & зависимое произведение $\prod$ \\
           квантор существования $\exists$ & зависимая сумма $\sum$ \\
        \end{tabular}
     \end{align*}

  \subsection{Особенности конкретных систем}

     Прежде чем рассмотреть различные proof assistants, необходимо определить понятия \emph{интерактивного} и \emph{автоматического} построения доказательства. \emph{Интерактивным} способом мы будем обозначать взаимодействие пользователя с системой на протяжении всего процесса с целью управления доказательством, а \emph{автоматическим} способом --- взаимодействие, полностью исключающее вмешательство пользователя, кроме формулирования цели (утверждения, теоремы).

  \subsubsection{Coq.}

     Одна из самых известных и зрелых систем для интерактивного доказательства теорем --- Coq\footnote{http://coq.inria.fr}. Как и все инструменты, рассмотренные в данной работе, Coq использует функциональный язык программирования с зависимыми типами --- Gallina --- для описания структур данных, определения функций и типов.

     Интерактивное и автоматическое доказательство теорем в Coq осуществляется с помощью \emph{тактик} --- программ для обработки контекста доказательства (контекст доказательства содержит переменные-гипотезы подобно контексту вычислений, содержащему переменные-значения). Тактики можно писать на специальном языке Ltac; вдобавок, есть встроенная библиотека тактик. Некоторые тактики способны полностью автоматически доказывать теоремы для алгоритмически разрешимых теорий (например, \emph{omega} для арифметики Пресбургера).

     Присутствует автоматизация и в автоматическом выводе типов --- можно опускать некоторые типы в сигнатурах функций, которые Coq может вычислить самостоятельно.

     Coq также позволяет разрабатывать и верифицировать программы на основе одного исходного кода, т.к. обладает механизмом извлечения кода на языках OCaml, Haskell и Scheme из исходных текстов Coq. При этом верификационная информация стирается для большей производительности.

  \subsubsection{Agda.}

     Система Agda\footnote{http://wiki.portal.chalmers.se/agda} более молодая и имеет меньше средств для автоматизации доказательств.

     В отличие от Coq механизма тактик в Agda нет, как и разделения доказательства на фазы формулировки и собственно доказательства. Вместо этого теоремы определяются как простые функции (из соответствия Карри-Говарда следует, что функции и доказательства теорем суть одно и то же). Однако отсутствие тактик в некоторой степени компенсируется \emph{рефлексией} в последних версиях системы, т.е. возможностью внутри доказательства обратиться к утверждению.

     В Agda реализована подсистема Agsy для автоматического поиска \emph{type inhabitant}, т.е. значения заданного типа. С помощью неё можно автоматически искать доказательства теорем, но этот инструмент недостаточно зрелый и имеет ряд ограничений.

     Кроме того, автоматически можно разбивать аргументы функций на конструкторы, что также автоматизирует построение доказательства.

  \section{Операционные семантики}

    \newcommand{\control}[2]{\langle #1, #2 \rangle}
    \newcommand{\rulens}[3]{\control{#1}{#2} \to #3}
    \newcommand{\ruless}[4]{\rulens{#1}{#2}{#3} \frac{#4}{}}
    \newcommand{\tree}[3]{\cfrac{#1 \hspace{10mm} #2}{#3}}

    \newcommand{\assign}[0]{\rulens{x:=a}{s}{s[x \mapsto a]}}
    \newcommand{\skipr}[0]{\rulens{skip}{s}{s}}

    \newcommand{\whilemacro}[0]{\mbox{while b do p}}

    \newcommand{\seqns}[0]{\tree{\rulens{p_1}{s_0}{s_1}}{\rulens{p_2}{s_1}{s_2}}{\rulens{p_1 ; p_2}{s_0}{s_2}}}
    \newcommand{\ifmacrons}[1]{\Rightarrow\tree{\rulens{p_#1}{s_0}{s_#1}}{}
                                                            {\rulens{\mbox{if b then $p_1$ else $p_2$}}{s_0}{s_#1}}}
    \newcommand{\iftruens}[0]{s_0[b] = true \ifmacrons{1}}
    \newcommand{\iffalsens}[0]{s_0[b] = false \ifmacrons{2}}
    \newcommand{\whiletruens}[0]{s_0[b] = true\Rightarrow\newline\indent\tree{\rulens{p}{s_0}{s_1}}{\rulens{\whilemacro}{s_1}{s_2}}
                                                            {\rulens{\whilemacro}{s_0}{s_2}}}
    \newcommand{\whilefalsens}[0]{s_0[b] = false\Rightarrow\rulens{\whilemacro}{s_0}{s_0}}

    \newcommand{\seqssn}[0]{\tree{\rulens{p_1}{s_0}{s_1}}{}{\ruless{p_1 ; p_2}{s_0}{s_1}{p_2}}}
    \newcommand{\seqssj}[0]{\tree{\ruless{p_1}{s_0}{s_1}{p_1'}}{}
                                 {\ruless{p_1 ; p_2}{s_0}{s_1}{p_1' ; p_2}}}
    \newcommand{\iftruess}[0]{s[b] = true\Rightarrow\ruless{\mbox{if b then $p_1$ else $p_2$}}{s}{s}{p_1}}
    \newcommand{\iffalsess}[0]{s[b] = false\Rightarrow\ruless{\mbox{if b then $p_1$ else $p_2$}}{s}{s}{p_2}}
    \newcommand{\whiless}[0]{\ruless{\whilemacro}{s}{s}{\mbox{if b then (p ; while b do p) else skip}}}

    \emph{Операционная семантика}\cite{Nielson:1992:SAF:129085} программы задаёт отношение на множестве состояний и определяется набором правил вывода.

    Обозначения следующие:
    \begin{align*}
       \begin{tabular}{ p{3cm} || p{6cm} }
          $<S; s> \to  s'$ & программа $S$ переводит состояние $s$ в состояние $s'$ \\
          \hline
          $s[k \mapsto v]$ & модификация состояния $s$                    \\
                           & присвоение значения $v$ переменной $k$       \\
          \hline
          $\tree{A}{B}{C}$ & составное правило                            \\
                           & A и B --- посылки, а C --- заключение        \\
        \end{tabular}
    \end{align*}

  \newcommand{\KWhile}[0]{{\bf While}}
  \subsection{Язык \KWhile}

    \newcommand{\Num}[0]{{\bf Num}}
    \newcommand{\Var}[0]{{\bf Var}}
    \newcommand{\Aexp}[0]{{\bf Aexp}}
    \newcommand{\Bexp}[0]{{\bf Bexp}}
    \newcommand{\Stm}[0]{{\bf Stm}}

    Примеры правил будут приведены для операционных семантик \emph{большого шага} и \emph{малого шага} для языка \KWhile\cite{Nielson:1992:SAF:129085}. Вкратце опишем синтаксис этого языка.

    Для языка \KWhile \ccode{ }определены следующие синтаксические категории и мета-переменные:
    \begin{itemize}
       \item категория \Num \ccode{ }из нумералов и мета-переменная $n$ для них;
       \item категория \Var \ccode{ }из переменных вместе с мета-переменной $x$;
       \item категория \Aexp, состоящая из арифметических выражений, и мета-переменная $a$;
       \item категория \Bexp, содержащая логические выражения, и мета-переменная $b$ для них;
       \item категория \Stm \ccode{ }инструкций языка \KWhile \ccode{ }и мета-переменная $S$.
    \end{itemize}
    
    Далее приведём синтаксис в форме Бэкуса --- Наура:

    $$
    \begin{array}{rcl}
      a&::=&n\mid x \mid a_1 + a_2 \mid a_1 * a_2 \mid a_1 - a_2\\
      b&::=&\ccode{true} \mid \ccode{false} \mid a_1 = a_2 \mid a_1 \leq a_2 \mid \neg b \mid b_1 \wedge b_2\\
      S&::=&x := a \mid \ccode{skip}  \mid S_1 \ccode{ ; } S_2\mid\\
       && \ccode{if } b_1 \ccode{ then } S_1 \ccode{ else } S_2 \mid \ccode{while } b \ccode{ do } S 
    \end{array}
    $$

  \subsection{Примеры правил}

    Приведём правила операционной семантики \emph{большого шага}:
    \begin{align*}
       \begin{tabular}{ p{1.5cm} || p{7.5cm} }
          ass (``:='') & $\assign$ \\
          \hline
          seq (``;'')  & $\seqns$ \\
          \hline
          skip         & $\skipr$ \\
          \hline
          if           & 1. $\iftruens$ \\
                       & 2. $\iffalsens$ \\
          \hline
          while        & 1. $\whiletruens$ \\
                       & 2. $\whilefalsens$ \\
       \end{tabular}
    \end{align*}

    Здесь \emph{ass}, \emph{skip}, \emph{while-2} --- элементарные правила, не требующие предпосылок, остальные --- составные.

    Таким образом, каждой программе соответствует \emph{семантическое дерево}, листья которого --- применения элементарных правил, а ветви --- посылки к составным.

    Кроме операционной семантики большого шага (она же \emph{натуральная} семантика) существует понятие операционной семантики \emph{малого шага}, или \emph{структурной}. В этой семантике переходам между состояниями разрешено иметь остаточную программу, за счёт чего упрощаются правила и исчезают правила с двумя посылками.
    \begin{align*}
       \begin{tabular}{ p{1.5cm} || p{7.5cm} }
          ass (``:='')  & $\assign$  \\
          \hline
          seq (``;'')   & 1. $\seqssn$ \\
                        & 2. $\seqssj$ \\
          \hline
          skip          & $\skipr$ \\
          \hline
          if            & 1. $\iftruess$  \\
                        & 2. $\iffalsess$ \\
          \hline
          while         & $\whiless$ \\
       \end{tabular}
    \end{align*}

    В семантике малого шага в каждой вершине семантического дерева скрыт список остаточных программ, а само дерево вырождено в список; новые узлы этого дерева появляются только благодаря правилам seq. В некотором смысле такое представление программы более структурировано, отсюда и второе название этой семантики.

    От натуральной семантики можно перейти к структурной, проигнорировав во всех правилах остаточную программу. В обратную сторону это также верно. В книге\cite{Nielson:1992:SAF:129085} доказано, что операционные семантики большого и малого шагов для языка \KWhile \ccode{ }эквивалентны.

  \section{Реализация интерпретатора операционной семантики}

  Рассмотрим поэтапно описание языка \KWhile \ccode{ }на Agda.

  \subsection{Синтаксис языка \KWhile}
     Абстрактный синтаксис языка определяется с помощью нескольких простых алгебраических типов данных без параметров. Исходный текст является фактически трансляцией записи Бэкуса --- Наура в Agda.

     В первую очередь, определим типы данных для алгебраических и логических выражений.
     \begin{lstlisting}
     data Aexp : Set where
       const : N -> Aexp
       var   : V -> Aexp
       plus  : Aexp -> Aexp -> Aexp
       minus : Aexp -> Aexp -> Aexp
       star  : Aexp -> Aexp -> Aexp
     \end{lstlisting}

     Здесь использован тип \lcode{V}; предполагается, что он определён заранее. Например, это может быть синоним для типа строк: \lcode{V = String}.

     \begin{lstlisting}
     data Bexp : Set where
       const : Bool -> Bexp
       conj  : Bexp -> Bexp -> Bexp
       neg   : Bexp -> Bexp
       lt    : Aexp -> Aexp -> Bexp
       eq    : Aexp -> Aexp -> Bexp
     \end{lstlisting}

     Затем определим тип операторов языка:
     \begin{lstlisting}
     data Stm : Set where
       skip   : Stm
       comp   : Stm  -> Stm  -> Stm
       assign : V    -> Aexp -> Stm
       while  : Bexp -> Stm  -> Stm
       branch : Bexp -> Stm  -> Stm -> Stm
     \end{lstlisting}

  \subsection{Семантика языка \KWhile}

  Для задания правил семантик нам понадобятся некоторые семантические операции вроде присвавивания значения переменной или вычисления арифметического выражения.

  Не будем приводить их определения, но укажем типы:
     \begin{align*}
        \small
        \begin{tabular}{l || r}
           \lstinline{_ |> _   : Binding -> State -> State} &
              установка значения переменной \\
           \lstinline{_ <| _   : State -> V -> N}           &
              получение значения переменной \\
           \lstinline{_ [[ _ ]] : State -> Aexp -> N}        &
              вычисление выражения \\
           \lstinline{_ << _ >> : State -> Bexp -> Bool}     & 
              вычисление выражения \\
        \end{tabular}
     \end{align*}

  Здесь \lcode{State} --- тип состояний вычисления, определённый как список переменных вместе с их значениями:
  \begin{lstlisting}
  record Binding : Set where
    constructor _,_
    field
      key   : V
      value : N

  State = List Binding
  \end{lstlisting}

  Правила операционной семантики мы зададим с помощью зависимого типа \lcode{Transition}. Значение этого типа является семантическим деревом некоторой программы и одновременно является доказательством того, что программа \emph{переводит} одно состояние в другое, т.е. завершает свою работу в некотором состоянии при заданном начальном состоянии. Конструкторы \lcode{Transition} кодируют метки вершин семантического дерева.

  Воспользуемся приёмом, описанным выше, и определим нужный нам тип как \emph{представление}, тогда мы сможем получать информацию о виде посылок правила при сопоставлении этого правила с образцом.

  Сигнатура типа (для натуральной семантики) выглядит следующим образом:
  \begin{lstlisting}
  Transition (`$s_1$` : State) : Stm -> State -> Set
  \end{lstlisting}
  
  Параметр $s_1$ фиксирован для всего типа в целом, что означает, что начальное состояние для программы задаётся извне и не зависит от самой программы. Остальные параметры не фиксированы: возможные программы и состояния, в которых они заканчиваются, зависят от меток дерева (конструкторов).

  Правила без посылок кодируются как следующие конструкторы:
  \begin{lstlisting}[mathescape]
  [skip]    : Transition `$s_1$` skip `$s_1$`
  [assign]  : $\forall$ {k v}
    -> Transition `$s_1$` (assign k v) ((k , `$s_1$` [[ v ]]) |> `$s_1$`)
  \end{lstlisting}
  Поскольку у элементарных правил нет посылок, то и аргументов у этих конструкторов нет.

  Остальные конструкторы:
  \begin{lstlisting}[mathescape]
  [comp]    :  $\forall$ {`$s_2$` `$s_3$` `$p_1$` `$p_2$`}
    -> Transition `$s_1$` `$p_1$` `$s_2$`
    -> Transition `$s_2$` `$p_2$` `$s_3$`
    -> Transition `$s_1$` (comp `$p_1$` `$p_2$`) `$s_3$`
  [if-t]    :  $\forall$ {`$s_2$` b `$p_1$` `$p_2$`} -> T (`$s_1$` << b >>)
    -> Transition `$s_1$` `$p_1$` `$s_2$`
    -> Transition `$s_1$` (branch b `$p_1$` `$p_2$`) `$s_2$`
  [if-f]    :  $\forall$ {`$s_2$` b `$p_1$` `$p_2$`} -> T (not (`$s_1$` << b >>))
    -> Transition `$s_1$` `$p_2$` `$s_2$`
    -> Transition `$s_1$` (branch b `$p_1$` `$p_2$`) `$s_2$`
  [while-t] :  $\forall$ {`$s_2$` `$s_3$` p} -> (b : B) -> T (`$s_1$` << b >>)
    -> Transition `$s_1$` p `$s_2$`
    -> Transition `$s_2$` (while b p) `$s_3$`
    -> Transition `$s_1$` (while b p) `$s_3$`
  [while-f] :  $\forall$ {p} -> (b : B) -> T (not (`$s_1$` << b >>))
    -> Transition `$s_1$` (while b p) `$s_1$`
  \end{lstlisting}

  При описании структурной семантики программа может завершиться с остаточной программой. Для выражения этого введём вспомогательный тип \lcode{Control} для состояний вместе с возможной остаточной программой и заменим второй параметр типа \lcode{State} в \lcode{Transition} на параметр типа \lcode{Control}.

  Код, необходимый для определения правил структурной семантики:
  \begin{lstlisting}[mathescape]
  record Control : Set where
    constructor [>_,_<]
    field
      state   : State
      program : Maybe S

  data Transition (`$s_1$` : State) : S -> Control -> Set where
    [skip]    : Transition `$s_1$` skip [> `$s_1$` , nothing <]
    [assign]  :  $\forall$ {k v }
      -> Transition `$s_1$` (assign k v)
        [> (k , `$s_1$` [[ v ]]) |> `$s_1$` , nothing <]
    [comp-j]  :  $\forall$ {`$s_2$` `$p_1$` `$p_2$` `$p_3$`}
      -> Transition `$s_1$` `$p_1$` [> `$s_2$` , just `$p_3$` <]
      -> Transition `$s_1$` (comp `$p_1$` `$p_2$`) [> `$s_2$` , just (comp `$p_3$` `$p_2$`) <]
    [comp-n]  :  $\forall$ {`$s_2$` `$p_1$` `$p_2$`   }
      -> Transition `$s_1$` `$p_1$` [> `$s_2$` , nothing <]
      -> Transition `$s_1$` (comp `$p_1$` `$p_2$`) [> `$s_2$` , just `$p_2$` <]
    [if-t]    :  $\forall$ (b : B) (`$p_1$` `$p_2$` : S) -> T (`$s_1$` << b >> )
      -> Transition   `$s_1$` (branch b `$p_1$` `$p_2$`) [> `$s_1$` , just `$p_1$` <]
    [if-f]    :  $\forall$ (b : B) (`$p_1$` `$p_2$` : S) -> T (not (`$s_1$` << b >>))
      -> Transition   `$s_1$` (branch b `$p_1$` `$p_2$`) [> `$s_1$` , just `$p_2$` <]
    [while-t] :  $\forall$ (b : B) (p : S) -> T (`$s_1$` << b >> )
      -> Transition `$s_1$` (while b p) [> `$s_1$` , just p <]
    [while-f] :  $\forall$ (b : B) (p : S) -> T (not (`$s_1$` << b >>))
      -> Transition `$s_1$` (while b p) [> `$s_1$` , nothing <]
  \end{lstlisting}

  Однако, теперь тип \lcode{Transition} задаёт более ``подробное'' отношение, чем нужно: оно определено также на тех значениях \lcode{Control}, символизирующих ``незавершённые'' вычисления, которые содержат остаточную программу. Поэтому определим дополнительно транзитивное замыкание этого отношения \lcode{Transition*} для выражения ``завершённых'' вычислений:
  \begin{lstlisting}[mathescape]
  data Transition* (`$s_1$` : State) : S -> State -> Set where
    cons :  $\forall$ {`$s_2$` `$s_3$` `$p_1$` `$p_2$`}
      -> Transition `$s_1$` `$p_1$` [> `$s_2$` , just `$p_2$` <]
      -> Transition* `$s_2$` `$p_2$` `$s_3$` -> Transition* `$s_1$` `$p_1$` `$s_3$`
    base :  $\forall$ {`$s_2$` p}
      -> Transition `$s_1$` p  [> `$s_2$` , nothing <]
      -> Transition* `$s_1$` p  `$s_2$`
  \end{lstlisting}
  В сущности, \lcode{Transition*} --- тип для списков семантических деревьев таких, что программа каждого следующего дерева является остаточной программой предыдущего.

  \subsection{Интерпретация программ}

  Интерпретатором программы мы будем называть функцию \lcode{interpret}, строящую семантическое дерево по данному состоянию и заданной программе. Тип этой функции должен быть \lcode{(s : State) -> (p : Stm) -> Interpretation s p}, где \lcode{Interpretation} --- пара, состоящая из конечного состояния и семантического дерева. Отдельный тип введён для того, чтобы выразить зависимость семантического дерева от конечного состояния.

  Определения \lcode{Interpretation} и \lcode{interpret}:
  \begin{lstlisting}
  record Interpretation (`$s_1$` : State) (p : Stm)
    : Set where
    constructor I_,_I
    field
      state      : State -- для` `структурной` `семантики` `Control
      transition : Transition `$s_1$` p state

  interpret : (s : State) -> (p : S)
    -> Interpretation s p
  \end{lstlisting}
  
  Такие типы называют \emph{зависимыми записями}.

  Семантическое дерево может быть бесконечного размера из-за таких правил как while. Поэтому функция \lcode{interpret} может работать бесконечно. Например, при обработке конструкции while необходимо рекурсивно вызывать \lcode{interpret} для одной и той же программы, нарушая принцип \emph{структурной рекурсии}. Поэтому мы не можем гарантировать завершаемость \lcode{interpret}.

  В то же время Agda по умолчанию производит проверку завершаемости (\emph{termination checking}) для всех своих программ. Следует выключить эту проверку для нашего интерпретатора.

  При этом, \lcode{interpret} для структурной семантики всегда завершается, т.к. вычисляет только один ``шаг'' программы, а остальную часть выдаёт в качестве остаточной программы. Необходимо реализовать также \lcode{interpret*} для вычисления замыкания \lcode{Transition*}. Для этой функции уже не гарантирована завершаемость, однако в отличие от семантики большого шага мы теперь разделили интерпретатор на две части по признаку завершаемости.

  Что касается реализации \lcode{interpret}, то существует возможность выполнить её интерактивно, используя механизмы разделения по случаям (\emph{case split}) и поиска значений типа.

  \noindent\begin{minipage}[c]{\linewidth}
  Эти механизмы позволяют в полу-автоматическом режиме развить незавершённое уравнение функции:
  \begin{lstlisting}
  interpret : (s : State) -> (p : S) -> Interpretation s p
  interpret s p = {!!} -- {!!} `--- `цель` `доказательства
  \end{lstlisting}
  в следующий код:
  \begin{lstlisting}
  interpret : (s : State) -> (p : S) -> Interpretation s p
  interpret `$s_1$` (skip) = I `$s_1$` , [skip] I
  interpret `$s_1$` (assign k v)
    = I (k , (`$s_1$` [[ v ]])) |> `$s_1$` , [assign] I
  interpret `$s_1$` (comp `$p_1$` `$p_2$`) with interpret `$s_1$` `$p_1$`
  ... | I `$s_2$` , `$tr_1$` I with interpret `$s_2$` `$p_2$`
  ... | I `$s_3$` , `$tr_2$` I = I `$s_3$` , [comp] `$tr_1$` `$tr_2$` I
  interpret `$s_1$` (branch b `$p_1$` `$p_2$`) with `$s_1$` << b >>
  | inspect (_<<_>> `$s_1$`) b
  | interpret `$s_1$` `$p_1$`
  | interpret `$s_1$` `$p_2$`
  ... | true  | Reveal_is_.[_] e | I `$s_2$` , `$tr_1$` I | I `$s_2$` , `$tr_2$` I
    = I `$s_2$` , [if-t] (trueIsTrue e) `$tr_1$` I
  ... | false | Reveal_is_.[_] e | I `$s_2$` , `$tr_1$` I | I `$s_2$` , `$tr_2$` I
    = I `$s_2$` , [if-f] (falseIsNotTrue e) `$tr_2$` I
  interpret `$s_1$` (while  b p) with `$s_1$` << b >>
  | inspect (_<<_>> `$s_1$`) b
  ... | false | Reveal_is_.[_] e
    = I `$s_1$` , [while-f] b (falseIsNotTrue e) I
  ... | true  | Reveal_is_.[_] e with interpret `$s_1$` p
  ... | I `$s_2$` , `$tr_1$` I with interpret `$s_2$` (while b p)
  ... | I `$s_3$` , `$tr_2$` I = I `$s_3$` , [while-t] b (trueIsTrue e) `$tr_1$` `$tr_2$` I
  \end{lstlisting}
  \end{minipage}

  Однако, к сожалению, эти механизмы не настолько зрелы, чтобы полностью автоматизировать реализацию. Поэтому приходится некоторые элементы реализовывать вручную. Здесь введен не-автоматически весь исходный текст, начинающийся ключевым словом \lcode{with} или содержащий конструктор \lcode{Reveal_is_.[_]}.

  В будущем ожидается, что в Agda появится возможность автоматически вводить \lcode{with}-выражения. Как альтернатива, возможно применение специальных \emph{элиминирующих} функций вместо \lcode{with}-выражений.

  \subsection{Доказательство свойств}

  Как пример утверждений о семантике языка, которые можно формулировать и доказывать с помощью построенного описания, приведём доказанный в \cite{Nielson:1992:SAF:129085} факт об эквивалентности семантик большого и малого шагов \KWhile.

  Для избежания конфликта имён, переименуем \lcode{Transition} в \lcode{Transition-NS} и \lcode{Transition-SS} для натуральной и структурной семантик соответственно. Транзитивное замыкание \lcode{Transition*} для структурной семантики переименуем в \lcode{Transition-SS*}.

  \noindent\begin{minipage}[c]{\linewidth}
  Запишем утверждение об эквивалентности в виде сигнатуры функции:
  \begin{lstlisting}[mathescape]
  ss=ns : (s : State) -> (p : S) ->  $\forall$ {s-ss s-ns}
      -> (tr-ss : Transition-SS* s p s-ss)
      -> (tr-ns : Transition-NS  s p s-ns)
      -> s-ss $\equiv$ s-ns
  \end{lstlisting}
  \end{minipage}

  Расшифровать тип этой функции можно следующим образом: для любых заданных состояний \lcode{s}, \lcode{s-ss}, \lcode{s-ns} и программе \lcode{p}, если есть семантические деревья \lcode{p} с начальным состоянием \lcode{s} и конечными состояниями \lcode{s-ns} и \lcode{s-ss} для натуральной и структурной семантик соответственно, то эти состояния \lcode{s-ns} и \lcode{s-ss} равны.

  Приведём доказательство этого утверждения для базового случая, когда после интерпретации в структурной семантике отсутствует остаточная программа:
  \begin{lstlisting}[mathescape]
  ss=ns-base : (s : State) -> (p : S) ->  $\forall$ {s-ss s-ns}
    -> (tr-ss : Transition-SS s p [> s-ss , nothing <])
    -> (tr-ns : Transition-NS s p    s-ns)
    -> s-ss $\equiv$ s-ns

  ss=ns-base  .s-ns .skip {.s-ns} {s-ns}
    [skip] [skip] = refl
  ss=ns-base   s    .(assign k v)
    ([assign] {k} {v}) [assign] = refl
  ss=ns-base  .s-ns .(while  b p) {.s-ns} {s-ns}
    ([while-f] b p x) ([while-f] .b `$x_1$`) = refl
  \end{lstlisting}

  Стоит заметить, что во всех уравнениях определения достаточно одного только \lcode{refl} (свойство рефлексивности равенства) в качестве правых частей. Однако надо правильным образом составить левые части, чтобы типизатор Agda мог убедиться в корректности.

  Разработка доказательства производилась с использованием тех же средств интерактивного доказательства, что и построение интерпретатора.

  \section*{Заключение}

  В ходе работы стало ясно, что proof assistants вполне применимы для описания операционных семантик. Удалось задать несколько семантик для тестового языка и построить для них интерпретаторы вместе с частичным доказательством их эквивалентности для данного языка.

  Получилось выполнить разработку интерактивно с использованием встроенных в Agda средств: разделения по случаям и автоматического поиска решений. Однако полностью автоматически провести построение не удалось. Планируется в дальнейшем опробовать другие средства, предоставляемые proof assistants, для достижения этой цели: тактики, рефлексию и прочее.

\begin{thebibliography}{99}
\bibitem{DBLP:conf/tldi/Norell09}
Ulf Norell. Dependently Typed Programming in Agda. International Workshop on Types in Language Design and Implementation, 2009.

%\bibitem{DBLP:conf/tldi/2009}
%Andrew Kennedy, Amal Ahmed. Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop
%               on Types in Languages Design and Implementation, Savannah,
%               GA, USA, January 24, 2009.

\bibitem{Pierce:2002:TPL:509043}
Benjamin C.Pierce. Types and Programming Languages. MIT Press, 2002.

\bibitem{Nielson:1992:SAF:129085}
Hanne Riis Nielson, Flemming Nielson. Semantics with Applications: a Formal Introduction. John Wiley \& Sons, Inc., 1992.

\bibitem{DBLP:journals/lisp/Strachey00}
Christopher Strachey. Fundamental Concepts in Programming Languages.
Higher-Order and Symbolic Computation, Vol. 13, No. 1/2, 2000. 
\end{thebibliography}
